A:Type, I:MaInterface(A), l:IdLnk, tg:Id, nmr:Namer(2;[tg; lname(l)] @ ma-interface-tags(I)).
Normal(A,I)
 gluable(I;l;tg)
 gluable2(A;I;l;tg)
 (x:Id.
 (x  filter(i.i = source(l);remove-repeats(IdDeq;ma-interface-locs(I))))
  (triggersGlue(A; (link nmr(0) from x to source(l)); (nmr(1)); ma-interface-ds(I;x); (I(x).2))
  ( Realizer)) 

latex

Definitions

x:A. B(x), (x  l), remove-repeats(eq;L), IdDeq, ma-interface-locs(I), P  Q, s = t, Id, t  T, a:A fp B(a), Knd, x:A  B(x), Type, State(ds), if b then t else f fi , ma-interface-loc(I;i), ma-interface-ds(I;i), source(l), , x:AB(x), left + right, Top, ma-interface-conds(I;i), filter(P;l), a = b, as @ bs, [car / cdr], lname(l), [], ma-interface-tags(I), , , False, Void, #$n, A  B, Unit, , b, , x.A(x), type List, x. t(x), a < b, gluable2(A;I;l;tg), gluable(I;l;tg), A, Normal(A,I), Normal(ds), Normal(T), Namer(n;Id_list), {x:A| B(x)} , Atom$n, IdLnk, MaInterface(T), b, P  Q, P & Q, s ~ t, strong-subtype(A;B), SQType(T), {T}, es-in-port-conds(A;l;tg), (link n from i to j), f(a), x:A. B(x), P  Q, i  j < k, {i..j}, case b of inl(x) => s(x) | inr(y) => t(y), T, True, f(x)?z, f  g, x:A.B(x), x  dom(f), KindDeq, Realizer, triggersGlue(A; l; tg; ds; conds), ma-interface-dom(I;i), S  T, hasloc(k;i), lsrc mk lnk compseq tag def

Lemmas

ma-interface-dom-hasloc, hasloc wf, ma-interface-dom wf, assert-deq-member, fpf-dom wf, triggersGlue wf, Kind-deq wf, es realizer wf, ma-interface-conds-equals, member filter, ma-interface-conds wf, fpf-empty-sub, subtype-fpf-cap-top, subtype rel self, fpf-cap wf, subtype rel dep function, subtype rel function, subtype rel product, subtype-fpf2, mk lnk wf, es-in-port-conds wf, assert-eq-id, not functionality wrt iff, ma-interface-conds wf3, Id sq, guard wf, member-remove-repeats, member wf, fpf wf, Knd wf, decl-state wf, top wf, assert-ma-interface-loc, l member subtype, ma-interface-ds wf, fpf-trivial-subtype-top, Id wf, fpf-empty wf, bool wf, lsrc wf, ma-interface-loc wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, ma-interface wf, IdLnk wf, le wf, ma-interface-tags wf, lname wf, append wf, Namer wf, ma-interface-normal wf, gluable wf, gluable2 wf, ma-interface-locs wf, id-deq wf, remove-repeats wf, eq id wf, filter wf, l member wf